(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a(x1) → x1
a(x1) → b(b(x1))
a(b(x1)) → a(c(a(c(x1))))
c(c(x1)) → x1

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3.
The certificate found is represented by the following graph.
Start state: 453
Accept states: [454, 455]
Transitions:
453→454[a_1|0, a_1|2]
453→455[c_1|0]
453→453[b_1|0]
453→456[b_1|1]
453→457[c_1|1]
453→461[b_1|2]
453→462[b_1|3]
456→454[b_1|1]
457→458[a_1|1]
457→460[b_1|2]
457→459[c_1|2]
458→459[c_1|1]
459→454[a_1|1]
459→461[b_1|2]
460→458[b_1|2]
461→454[b_1|2]
462→454[b_1|3]

(2) BOUNDS(O(1), O(n^1))